module digitalpolitic

//Definizione dei tipi base

open util/boolean
open util/ordering[Data]

sig Stringa {}
sig Data{}
sig Hash {}
sig Crc {}
sig Email{}

//1. Elementi del Sistema

sig ElectionDay{
data:one Data,
nome:one Stringa,
}

sig PeriodoElettorale{
nome:one Stringa,
electionDay:one ElectionDay,
dataInizio:one Data,
dataFine:one Data,
}{
lt[dataInizio, dataFine]
}

sig Candidatura{
utente:one Utente,
partito:one Partito,
}

sig Partito{
nome:one Stringa,
}

sig VotoDiPartito{
membro:one Membro,
candidatura:one Candidatura,
}

sig VotoDiStato{
votante: one Utente,
electionDay: one ElectionDay,
partito : one Partito,
candidati : some Membro,
}{
	#candidati<4
}
// 2. Utenti del sistema

sig Utente {
crc: one Crc,
nome:one Stringa,
cognome:one Stringa,
email:one Email,
password:one Hash,
}

sig Membro extends Utente{
partito:one Partito,
}

sig Incaricato extends Utente {}

sig Amministratore extends Utente {}

//Fatti

fact almenoDuePartiti{
	#Partito>1
}

fact noPartitiStessoNome{
	no disj p1,p2 : Partito | p1.nome=p2.nome
}

fact noUtentiStessaMail{
	no disj p1,p2 : Utente | p1.email=p2.email
}

fact noUtentiStessoCrc{
	no disj p1,p2 : Utente | p1.crc=p2.crc
}

fact noPiùCandidature{
	no disj p1,p2 : Candidatura | p1.utente = p2.utente
}

fact noMembroCandidato{
no p2:Candidatura | p2.utente = Membro
}

fact almenoUnIncaricato {
	#Incaricato > 0
}
fact almenoUnAmministratore {
	#Amministratore > 0
}

fact noElectionDayStessoNomeStessaData {
	no disj p1,p2: ElectionDay | p1.nome = p2.nome and p1.data = p2.data
}

fact noDuePeriodiElettoraliStessoElectionDay{
	no disj p1,p2:PeriodoElettorale | p1.electionDay = p2.electionDay
}

fact votoDiPartitoSoloMembri{
	all p1:VotoDiPartito | p1.membro.partito = p1.candidatura.partito
}

fact votoDiStatoSoloUnaVolta{
	no disj p1,p2:VotoDiStato | p1.electionDay = p2.electionDay and p1.votante=p2.votante
}

fact soloMembriDelPartito{
	all p1:VotoDiStato | p1.candidati.partito = p1.partito
}

pred show{}

run show{}

